Nuprl Lemma : void-list-equality
11,40
postcript
pdf
x
,
y
:(Void List).
x
~
y
latex
Definitions
t
T
,
Void
,
type
List
,
x
:
A
B
(
x
)
,
s
~
t
,
x
:
A
.
B
(
x
)
origin
x, y:(Void List). x ~ y x, y:(Void List). x ~ y 
T
B(x)x:A. B(x)